Inference at * 1 2 1 
Iof proof for Lemma p-fun-exp-add1-sq:

.....truecase..... NILNIL

1. A : Type
2. f : A(A + Top)
3. x : A
4. isl(f(x))
5. n : 
6. 0 < n
7. (primrec(n - 1;f o p-id()  ;i,g. f o g  )(x))
7. ~
7. (primrec(n - 1;p-id();i,g. f o g  )(outl(f(x))))
8. n = 0
  (f o p-id()  (x)) ~ (p-id()(outl(f(x)))) 

latex

 by Auto' 

latex

 .

Definitions

s ~ t